1. Technical Field
The present invention relates generally to a method, system, and computer program product for creating electronic circuits. More particularly, the present invention relates to a method, system, and computer program product for improved model checking in the verification of a hardware design implementing a state transition machine.
2. Description of the Related Art
Electronic circuits can be configured to perform mathematical computations. For example, a logic circuit in a microprocessor's integrated circuit may be configured to multiply two integers by manipulating their binary representation in a series of steps according to an algorithm.
Before the circuit can be designed for performing a computation, the series of steps according to a corresponding algorithm are represented in the form of a state transition machine (STM). A state transition machine is also known as a finite state machine, a finite state automaton, or simply a state machine.
A STM includes a set of states. A transition from one state to another state is called a state transition, and occurs in the STM when certain conditions are met. A state can receive an input, and produce an output. The output of one state may be an input for another state. Conditions that exist before a state transition are called pre-conditions. Conditions that exist after a state transition occurs are called post-conditions. For example, an input and pre-conditions trigger the operation of a STM, which performs state transitions according to the conditions configured in the STM, and produces an output and post-conditions.
Operating a STM is the process of supplying the STM an input and a set of pre-conditions, performing state transitions of the STM, and generating an output and post-conditions. Depending on the conditions programmed for the various state transitions, operating a STM can take a significant amount of time. A STM taking several seconds, typically a billion machine cycles or more, to generate an output is not uncommon.
The operation of a STM can be further affected by the size of data used in the operation. For example, where a STM may perform a computation using sixty four bit inputs in a matter of nano-seconds, the same STM may take many seconds to perform the same operation using eight thousand bit inputs.